<!DOCTYPE HTML PUBLIC "-//W3C//DTD HTML 4.01 Transitional//EN" "http://www.w3.org/TR/html4/loose.dtd">
<!-- NewPage -->
<html lang="en">
<head>
<title>Assrt</title>
<link rel="stylesheet" type="text/css" href="../../stylesheet.css" title="Style">
</head>
<body>
<script type="text/javascript"><!--
    if (location.href.indexOf('is-external=true') == -1) {
        parent.document.title="Assrt";
    }
//-->
</script>
<noscript>
<div>JavaScript is disabled on your browser.</div>
</noscript>
<!-- ========= START OF TOP NAVBAR ======= -->
<div class="topNav"><a name="navbar_top">
<!--   -->
</a><a href="#skip-navbar_top" title="Skip navigation links"></a><a name="navbar_top_firstrow">
<!--   -->
</a>
<ul class="navList" title="Navigation">
<li><a href="../../overview-summary.html">Overview</a></li>
<li><a href="package-summary.html">Package</a></li>
<li class="navBarCell1Rev">Class</li>
<li><a href="package-tree.html">Tree</a></li>
<li><a href="../../deprecated-list.html">Deprecated</a></li>
<li><a href="../../index-all.html">Index</a></li>
<li><a href="../../help-doc.html">Help</a></li>
</ul>
</div>
<div class="subNav">
<ul class="navList">
<li>Prev Class</li>
<li><a href="../../mmj/lang/Axiom.html" title="class in mmj.lang"><span class="strong">Next Class</span></a></li>
</ul>
<ul class="navList">
<li><a href="../../index.html?mmj/lang/Assrt.html" target="_top">Frames</a></li>
<li><a href="Assrt.html" target="_top">No Frames</a></li>
</ul>
<ul class="navList" id="allclasses_navbar_top">
<li><a href="../../allclasses-noframe.html">All Classes</a></li>
</ul>
<div>
<script type="text/javascript"><!--
  allClassesLink = document.getElementById("allclasses_navbar_top");
  if(window==top) {
    allClassesLink.style.display = "block";
  }
  else {
    allClassesLink.style.display = "none";
  }
  //-->
</script>
</div>
<div>
<ul class="subNavList">
<li>Summary:&nbsp;</li>
<li>Nested&nbsp;|&nbsp;</li>
<li><a href="#field_summary">Field</a>&nbsp;|&nbsp;</li>
<li><a href="#constructor_summary">Constr</a>&nbsp;|&nbsp;</li>
<li><a href="#method_summary">Method</a></li>
</ul>
<ul class="subNavList">
<li>Detail:&nbsp;</li>
<li><a href="#field_detail">Field</a>&nbsp;|&nbsp;</li>
<li><a href="#constructor_detail">Constr</a>&nbsp;|&nbsp;</li>
<li><a href="#method_detail">Method</a></li>
</ul>
</div>
<a name="skip-navbar_top">
<!--   -->
</a></div>
<!-- ========= END OF TOP NAVBAR ========= -->
<!-- ======== START OF CLASS DATA ======== -->
<div class="header">
<div class="subTitle">mmj.lang</div>
<h2 title="Class Assrt" class="title">Class Assrt</h2>
</div>
<div class="contentContainer">
<ul class="inheritance">
<li>java.lang.Object</li>
<li>
<ul class="inheritance">
<li><a href="../../mmj/lang/MObj.html" title="class in mmj.lang">mmj.lang.MObj</a></li>
<li>
<ul class="inheritance">
<li><a href="../../mmj/lang/Stmt.html" title="class in mmj.lang">mmj.lang.Stmt</a></li>
<li>
<ul class="inheritance">
<li>mmj.lang.Assrt</li>
</ul>
</li>
</ul>
</li>
</ul>
</li>
</ul>
<div class="description">
<ul class="blockList">
<li class="blockList">
<dl>
<dt>Direct Known Subclasses:</dt>
<dd><a href="../../mmj/lang/Axiom.html" title="class in mmj.lang">Axiom</a>, <a href="../../mmj/lang/Theorem.html" title="class in mmj.lang">Theorem</a></dd>
</dl>
<hr>
<br>
<pre>public abstract class <span class="strong">Assrt</span>
extends <a href="../../mmj/lang/Stmt.html" title="class in mmj.lang">Stmt</a></pre>
<div class="block">Assrt is an "Assertion", of which there are two main kinds, Axiom and Theorem
 -- known in Metamath as "Axiomatic Assertions" and "Provable Assertions".
 What do Assertions have in common that Hypotheses do not? "Mandatory" Frames.</div>
<dl><dt><span class="strong">See Also:</span></dt><dd><a href="../../MetamathERNotes.html"> Nomenclature and
      Entity-Relationship Notes</a></dd></dl>
</li>
</ul>
</div>
<div class="summary">
<ul class="blockList">
<li class="blockList">
<!-- =========== FIELD SUMMARY =========== -->
<ul class="blockList">
<li class="blockList"><a name="field_summary">
<!--   -->
</a>
<h3>Field Summary</h3>
<table class="overviewSummary" border="0" cellpadding="3" cellspacing="0" summary="Field Summary table, listing fields, and an explanation">
<caption><span>Fields</span><span class="tabEnd">&nbsp;</span></caption>
<tr>
<th class="colFirst" scope="col">Modifier and Type</th>
<th class="colLast" scope="col">Field and Description</th>
</tr>
<tr class="altColor">
<td class="colFirst"><code>protected <a href="../../mmj/lang/LogHyp.html" title="class in mmj.lang">LogHyp</a>[]</code></td>
<td class="colLast"><code><strong><a href="../../mmj/lang/Assrt.html#logHypArray">logHypArray</a></strong></code>
<div class="block">logHypArray contains *exactly* the Assrt's Formula's LogHyp's, in
 database sequence.</div>
</td>
</tr>
<tr class="rowColor">
<td class="colFirst"><code>protected <a href="../../mmj/lang/ScopeFrame.html" title="class in mmj.lang">ScopeFrame</a></code></td>
<td class="colLast"><code><strong><a href="../../mmj/lang/Assrt.html#mandFrame">mandFrame</a></strong></code>
<div class="block">The assertion's Mandatory Frame.</div>
</td>
</tr>
<tr class="altColor">
<td class="colFirst"><code>static java.util.Comparator&lt;<a href="../../mmj/lang/Assrt.html" title="class in mmj.lang">Assrt</a>&gt;</code></td>
<td class="colLast"><code><strong><a href="../../mmj/lang/Assrt.html#NBR_LOG_HYP_SEQ">NBR_LOG_HYP_SEQ</a></strong></code>
<div class="block">NBR_LOG_HYP_SEQ sequences by Stmt.seq</div>
</td>
</tr>
<tr class="rowColor">
<td class="colFirst"><code>protected <a href="../../mmj/lang/LogHyp.html" title="class in mmj.lang">LogHyp</a>[]</code></td>
<td class="colLast"><code><strong><a href="../../mmj/lang/Assrt.html#sortedLogHypArray">sortedLogHypArray</a></strong></code>
<div class="block">sortedLogHypArray contains the contents of logHypArray as sorted by
 loadSortedLogHypArray().</div>
</td>
</tr>
<tr class="altColor">
<td class="colFirst"><code>protected <a href="../../mmj/lang/VarHyp.html" title="class in mmj.lang">VarHyp</a>[]</code></td>
<td class="colLast"><code><strong><a href="../../mmj/lang/Assrt.html#varHypArray">varHypArray</a></strong></code>
<div class="block">varHypArray contains *exactly* the Assrt's Formula's VarHyp's, in
 database sequence.</div>
</td>
</tr>
</table>
<ul class="blockList">
<li class="blockList"><a name="fields_inherited_from_class_mmj.lang.Stmt">
<!--   -->
</a>
<h3>Fields inherited from class&nbsp;mmj.lang.<a href="../../mmj/lang/Stmt.html" title="class in mmj.lang">Stmt</a></h3>
<code><a href="../../mmj/lang/Stmt.html#DESC_NBR_PROOF_REFS">DESC_NBR_PROOF_REFS</a>, <a href="../../mmj/lang/Stmt.html#exprParseTree">exprParseTree</a>, <a href="../../mmj/lang/Stmt.html#LABEL">LABEL</a>, <a href="../../mmj/lang/Stmt.html#logHypsL1HiLoKey">logHypsL1HiLoKey</a>, <a href="../../mmj/lang/Stmt.html#logHypsMaxDepth">logHypsMaxDepth</a>, <a href="../../mmj/lang/Stmt.html#nbrProofRefs">nbrProofRefs</a></code></li>
</ul>
<ul class="blockList">
<li class="blockList"><a name="fields_inherited_from_class_mmj.lang.MObj">
<!--   -->
</a>
<h3>Fields inherited from class&nbsp;mmj.lang.<a href="../../mmj/lang/MObj.html" title="class in mmj.lang">MObj</a></h3>
<code><a href="../../mmj/lang/MObj.html#chapterNbr">chapterNbr</a>, <a href="../../mmj/lang/MObj.html#description">description</a>, <a href="../../mmj/lang/MObj.html#isTempObject">isTempObject</a>, <a href="../../mmj/lang/MObj.html#SECTION_AND_MOBJ_NBR">SECTION_AND_MOBJ_NBR</a>, <a href="../../mmj/lang/MObj.html#sectionMObjNbr">sectionMObjNbr</a>, <a href="../../mmj/lang/MObj.html#sectionNbr">sectionNbr</a>, <a href="../../mmj/lang/MObj.html#seq">seq</a>, <a href="../../mmj/lang/MObj.html#SEQ">SEQ</a></code></li>
</ul>
</li>
</ul>
<!-- ======== CONSTRUCTOR SUMMARY ======== -->
<ul class="blockList">
<li class="blockList"><a name="constructor_summary">
<!--   -->
</a>
<h3>Constructor Summary</h3>
<table class="overviewSummary" border="0" cellpadding="3" cellspacing="0" summary="Constructor Summary table, listing constructors, and an explanation">
<caption><span>Constructors</span><span class="tabEnd">&nbsp;</span></caption>
<tr>
<th class="colOne" scope="col">Constructor and Description</th>
</tr>
<tr class="altColor">
<td class="colOne"><code><strong><a href="../../mmj/lang/Assrt.html#Assrt(int, java.util.List, java.util.Map, java.util.Map, java.lang.String, java.lang.String, java.util.List)">Assrt</a></strong>(int&nbsp;seq,
     java.util.List&lt;<a href="../../mmj/lang/ScopeDef.html" title="class in mmj.lang">ScopeDef</a>&gt;&nbsp;scopeDefList,
     java.util.Map&lt;java.lang.String,<a href="../../mmj/lang/Sym.html" title="class in mmj.lang">Sym</a>&gt;&nbsp;symTbl,
     java.util.Map&lt;java.lang.String,<a href="../../mmj/lang/Stmt.html" title="class in mmj.lang">Stmt</a>&gt;&nbsp;stmtTbl,
     java.lang.String&nbsp;labelS,
     java.lang.String&nbsp;typS,
     java.util.List&lt;java.lang.String&gt;&nbsp;symList)</code>
<div class="block">Construct using a boatload of parameters.</div>
</td>
</tr>
</table>
</li>
</ul>
<!-- ========== METHOD SUMMARY =========== -->
<ul class="blockList">
<li class="blockList"><a name="method_summary">
<!--   -->
</a>
<h3>Method Summary</h3>
<table class="overviewSummary" border="0" cellpadding="3" cellspacing="0" summary="Method Summary table, listing methods, and an explanation">
<caption><span>Methods</span><span class="tabEnd">&nbsp;</span></caption>
<tr>
<th class="colFirst" scope="col">Modifier and Type</th>
<th class="colLast" scope="col">Method and Description</th>
</tr>
<tr class="altColor">
<td class="colFirst"><code>static &lt;T extends <a href="../../mmj/lang/Hyp.html" title="class in mmj.lang">Hyp</a>&gt;&nbsp;<br>void</code></td>
<td class="colLast"><code><strong><a href="../../mmj/lang/Assrt.html#accumHypInList(java.util.List, T)">accumHypInList</a></strong>(java.util.List&lt;T&gt;&nbsp;hypList,
              T&nbsp;hypNew)</code>
<div class="block">Accumulate unique hypotheses (no duplicates), storing them in an array
 list in order of their appearance in the database.</div>
</td>
</tr>
<tr class="rowColor">
<td class="colFirst"><code><a href="../../mmj/lang/LogHyp.html" title="class in mmj.lang">LogHyp</a>[]</code></td>
<td class="colLast"><code><strong><a href="../../mmj/lang/Assrt.html#getLogHypArray()">getLogHypArray</a></strong>()</code>
<div class="block">Return the logHypArray.</div>
</td>
</tr>
<tr class="altColor">
<td class="colFirst"><code>int</code></td>
<td class="colLast"><code><strong><a href="../../mmj/lang/Assrt.html#getLogHypArrayLength()">getLogHypArrayLength</a></strong>()</code>
<div class="block">Return the logHypArray length</div>
</td>
</tr>
<tr class="rowColor">
<td class="colFirst"><code>java.lang.String</code></td>
<td class="colLast"><code><strong><a href="../../mmj/lang/Assrt.html#getLogHypsL1HiLoKey()">getLogHypsL1HiLoKey</a></strong>()</code>
<div class="block">Dynamically computes, if needed, the Hi and Lo keys of Level 1 (root) of
 parse trees of logHypArray, and caches the value for later use.</div>
</td>
</tr>
<tr class="altColor">
<td class="colFirst"><code>int</code></td>
<td class="colLast"><code><strong><a href="../../mmj/lang/Assrt.html#getLogHypsMaxDepth()">getLogHypsMaxDepth</a></strong>()</code>
<div class="block">Dynamically computes, if needed, the larges maximum depth of parse trees
 of logHypArray, and caches the value for later use.</div>
</td>
</tr>
<tr class="rowColor">
<td class="colFirst"><code><a href="../../mmj/lang/ScopeFrame.html" title="class in mmj.lang">ScopeFrame</a></code></td>
<td class="colLast"><code><strong><a href="../../mmj/lang/Assrt.html#getMandFrame()">getMandFrame</a></strong>()</code>
<div class="block">Get the Assrt's MandFrame.</div>
</td>
</tr>
<tr class="altColor">
<td class="colFirst"><code>int</code></td>
<td class="colLast"><code><strong><a href="../../mmj/lang/Assrt.html#getMandHypArrayLength()">getMandHypArrayLength</a></strong>()</code>
<div class="block">Return the *mandatory* Hyp Array.Length</div>
</td>
</tr>
<tr class="rowColor">
<td class="colFirst"><code><a href="../../mmj/lang/VarHyp.html" title="class in mmj.lang">VarHyp</a>[]</code></td>
<td class="colLast"><code><strong><a href="../../mmj/lang/Assrt.html#getMandVarHypArray()">getMandVarHypArray</a></strong>()</code>
<div class="block">Return the *mandatory* varHypArray.</div>
</td>
</tr>
<tr class="altColor">
<td class="colFirst"><code><a href="../../mmj/lang/LogHyp.html" title="class in mmj.lang">LogHyp</a>[]</code></td>
<td class="colLast"><code><strong><a href="../../mmj/lang/Assrt.html#getSortedLogHypArray()">getSortedLogHypArray</a></strong>()</code>
<div class="block">Return the sortedLogHypArray.</div>
</td>
</tr>
<tr class="rowColor">
<td class="colFirst"><code>boolean</code></td>
<td class="colLast"><code><strong><a href="../../mmj/lang/Assrt.html#isActive()">isActive</a></strong>()</code>
<div class="block">Is the Assrt "active".</div>
</td>
</tr>
<tr class="altColor">
<td class="colFirst"><code>void</code></td>
<td class="colLast"><code><strong><a href="../../mmj/lang/Assrt.html#loadLogHypArray()">loadLogHypArray</a></strong>()</code>
<div class="block">Loads the logHypArray using mandFrame.</div>
</td>
</tr>
<tr class="rowColor">
<td class="colFirst"><code>void</code></td>
<td class="colLast"><code><strong><a href="../../mmj/lang/Assrt.html#setLogHypArray(mmj.lang.LogHyp[])">setLogHypArray</a></strong>(<a href="../../mmj/lang/LogHyp.html" title="class in mmj.lang">LogHyp</a>[]&nbsp;logHypArray)</code>
<div class="block">Set the logHypArray.</div>
</td>
</tr>
<tr class="altColor">
<td class="colFirst"><code>void</code></td>
<td class="colLast"><code><strong><a href="../../mmj/lang/Assrt.html#setMandFrame(mmj.lang.ScopeFrame)">setMandFrame</a></strong>(<a href="../../mmj/lang/ScopeFrame.html" title="class in mmj.lang">ScopeFrame</a>&nbsp;mandFrame)</code>
<div class="block">Set the Assrt's MandFrame.</div>
</td>
</tr>
<tr class="rowColor">
<td class="colFirst"><code>void</code></td>
<td class="colLast"><code><strong><a href="../../mmj/lang/Assrt.html#setMandVarHypArray(mmj.lang.VarHyp[])">setMandVarHypArray</a></strong>(<a href="../../mmj/lang/VarHyp.html" title="class in mmj.lang">VarHyp</a>[]&nbsp;varHypArray)</code>
<div class="block">Set the *mandatory* VarHyp Array.</div>
</td>
</tr>
<tr class="altColor">
<td class="colFirst"><code>static <a href="../../mmj/lang/Assrt.html" title="class in mmj.lang">Assrt</a>[]</code></td>
<td class="colLast"><code><strong><a href="../../mmj/lang/Assrt.html#sortListIntoArray(java.util.List, java.util.Comparator)">sortListIntoArray</a></strong>(java.util.List&lt;<a href="../../mmj/lang/Assrt.html" title="class in mmj.lang">Assrt</a>&gt;&nbsp;assrtList,
                 java.util.Comparator&lt;<a href="../../mmj/lang/Assrt.html" title="class in mmj.lang">Assrt</a>&gt;&nbsp;comparator)</code>
<div class="block">Sorts a list of Assrt into an array.</div>
</td>
</tr>
</table>
<ul class="blockList">
<li class="blockList"><a name="methods_inherited_from_class_mmj.lang.Stmt">
<!--   -->
</a>
<h3>Methods inherited from class&nbsp;mmj.lang.<a href="../../mmj/lang/Stmt.html" title="class in mmj.lang">Stmt</a></h3>
<code><a href="../../mmj/lang/Stmt.html#equals(java.lang.Object)">equals</a>, <a href="../../mmj/lang/Stmt.html#getExprParseTree()">getExprParseTree</a>, <a href="../../mmj/lang/Stmt.html#getExprRPN()">getExprRPN</a>, <a href="../../mmj/lang/Stmt.html#getFormula()">getFormula</a>, <a href="../../mmj/lang/Stmt.html#getLabel()">getLabel</a>, <a href="../../mmj/lang/Stmt.html#getNbrProofRefs()">getNbrProofRefs</a>, <a href="../../mmj/lang/Stmt.html#getTyp()">getTyp</a>, <a href="../../mmj/lang/Stmt.html#hashCode()">hashCode</a>, <a href="../../mmj/lang/Stmt.html#incrementNbrProofRefs()">incrementNbrProofRefs</a>, <a href="../../mmj/lang/Stmt.html#initNbrProofRefs()">initNbrProofRefs</a>, <a href="../../mmj/lang/Stmt.html#renderParsedSubExpr(java.lang.StringBuilder, int, int, mmj.lang.ParseNode[])">renderParsedSubExpr</a>, <a href="../../mmj/lang/Stmt.html#resetLogHypsL1HiLoKey()">resetLogHypsL1HiLoKey</a>, <a href="../../mmj/lang/Stmt.html#resetLogHypsMaxDepth()">resetLogHypsMaxDepth</a>, <a href="../../mmj/lang/Stmt.html#setExprParseTree(mmj.lang.ParseTree)">setExprParseTree</a>, <a href="../../mmj/lang/Stmt.html#setExprRPN(mmj.lang.ParseTree.RPNStep[])">setExprRPN</a>, <a href="../../mmj/lang/Stmt.html#setLogHypsL1HiLoKey(java.lang.String)">setLogHypsL1HiLoKey</a>, <a href="../../mmj/lang/Stmt.html#setLogHypsMaxDepth(int)">setLogHypsMaxDepth</a>, <a href="../../mmj/lang/Stmt.html#setTyp(mmj.lang.Cnst)">setTyp</a>, <a href="../../mmj/lang/Stmt.html#toString()">toString</a></code></li>
</ul>
<ul class="blockList">
<li class="blockList"><a name="methods_inherited_from_class_mmj.lang.MObj">
<!--   -->
</a>
<h3>Methods inherited from class&nbsp;mmj.lang.<a href="../../mmj/lang/MObj.html" title="class in mmj.lang">MObj</a></h3>
<code><a href="../../mmj/lang/MObj.html#getChapterNbr()">getChapterNbr</a>, <a href="../../mmj/lang/MObj.html#getDescription()">getDescription</a>, <a href="../../mmj/lang/MObj.html#getDescriptionForSearch()">getDescriptionForSearch</a>, <a href="../../mmj/lang/MObj.html#getIsTempObject()">getIsTempObject</a>, <a href="../../mmj/lang/MObj.html#getOrigSectionNbr()">getOrigSectionNbr</a>, <a href="../../mmj/lang/MObj.html#getSectionMObjNbr()">getSectionMObjNbr</a>, <a href="../../mmj/lang/MObj.html#getSectionNbr()">getSectionNbr</a>, <a href="../../mmj/lang/MObj.html#getSeq()">getSeq</a>, <a href="../../mmj/lang/MObj.html#setChapterNbr(int)">setChapterNbr</a>, <a href="../../mmj/lang/MObj.html#setDescription(java.lang.String)">setDescription</a>, <a href="../../mmj/lang/MObj.html#setIsTempObject(boolean)">setIsTempObject</a>, <a href="../../mmj/lang/MObj.html#setSectionMObjNbr(int)">setSectionMObjNbr</a>, <a href="../../mmj/lang/MObj.html#setSectionNbr(int)">setSectionNbr</a></code></li>
</ul>
<ul class="blockList">
<li class="blockList"><a name="methods_inherited_from_class_java.lang.Object">
<!--   -->
</a>
<h3>Methods inherited from class&nbsp;java.lang.Object</h3>
<code>clone, finalize, getClass, notify, notifyAll, wait, wait, wait</code></li>
</ul>
</li>
</ul>
</li>
</ul>
</div>
<div class="details">
<ul class="blockList">
<li class="blockList">
<!-- ============ FIELD DETAIL =========== -->
<ul class="blockList">
<li class="blockList"><a name="field_detail">
<!--   -->
</a>
<h3>Field Detail</h3>
<a name="varHypArray">
<!--   -->
</a>
<ul class="blockList">
<li class="blockList">
<h4>varHypArray</h4>
<pre>protected&nbsp;<a href="../../mmj/lang/VarHyp.html" title="class in mmj.lang">VarHyp</a>[] varHypArray</pre>
<div class="block">varHypArray contains *exactly* the Assrt's Formula's VarHyp's, in
 database sequence.
 <p>
 varHypArray is an array of length zero if the Assrt's Formula contains no
 variables.
 <p>
 Note: varHypArray is somewhat redundant, but note that MandFrame contains
 not only VarHyp's used in an Expression's Formula, but the LogHyp's that
 are in scope, <b>and the VarHyp's used by those LogHyp's!</b>.
 <p></div>
</li>
</ul>
<a name="logHypArray">
<!--   -->
</a>
<ul class="blockList">
<li class="blockList">
<h4>logHypArray</h4>
<pre>protected&nbsp;<a href="../../mmj/lang/LogHyp.html" title="class in mmj.lang">LogHyp</a>[] logHypArray</pre>
<div class="block">logHypArray contains *exactly* the Assrt's Formula's LogHyp's, in
 database sequence.
 <p>
 logHypArray is an array of length zero if the Assrt has no LogHyp's.
 <p>
 logHypArray is redundant with the data in ScopeFrame, but ProofAsst needs
 quick access to the LogHyp's as well as the actual number of LogHyp's.
 <p></div>
</li>
</ul>
<a name="sortedLogHypArray">
<!--   -->
</a>
<ul class="blockList">
<li class="blockList">
<h4>sortedLogHypArray</h4>
<pre>protected&nbsp;<a href="../../mmj/lang/LogHyp.html" title="class in mmj.lang">LogHyp</a>[] sortedLogHypArray</pre>
<div class="block">sortedLogHypArray contains the contents of logHypArray as sorted by
 loadSortedLogHypArray().
 <p>
 The sorted LogHyps are for the benefit of ProofAssistant.</div>
</li>
</ul>
<a name="mandFrame">
<!--   -->
</a>
<ul class="blockList">
<li class="blockList">
<h4>mandFrame</h4>
<pre>protected&nbsp;<a href="../../mmj/lang/ScopeFrame.html" title="class in mmj.lang">ScopeFrame</a> mandFrame</pre>
<div class="block">The assertion's Mandatory Frame.</div>
</li>
</ul>
<a name="NBR_LOG_HYP_SEQ">
<!--   -->
</a>
<ul class="blockListLast">
<li class="blockList">
<h4>NBR_LOG_HYP_SEQ</h4>
<pre>public static final&nbsp;java.util.Comparator&lt;<a href="../../mmj/lang/Assrt.html" title="class in mmj.lang">Assrt</a>&gt; NBR_LOG_HYP_SEQ</pre>
<div class="block">NBR_LOG_HYP_SEQ sequences by Stmt.seq</div>
</li>
</ul>
</li>
</ul>
<!-- ========= CONSTRUCTOR DETAIL ======== -->
<ul class="blockList">
<li class="blockList"><a name="constructor_detail">
<!--   -->
</a>
<h3>Constructor Detail</h3>
<a name="Assrt(int, java.util.List, java.util.Map, java.util.Map, java.lang.String, java.lang.String, java.util.List)">
<!--   -->
</a>
<ul class="blockListLast">
<li class="blockList">
<h4>Assrt</h4>
<pre>public&nbsp;Assrt(int&nbsp;seq,
     java.util.List&lt;<a href="../../mmj/lang/ScopeDef.html" title="class in mmj.lang">ScopeDef</a>&gt;&nbsp;scopeDefList,
     java.util.Map&lt;java.lang.String,<a href="../../mmj/lang/Sym.html" title="class in mmj.lang">Sym</a>&gt;&nbsp;symTbl,
     java.util.Map&lt;java.lang.String,<a href="../../mmj/lang/Stmt.html" title="class in mmj.lang">Stmt</a>&gt;&nbsp;stmtTbl,
     java.lang.String&nbsp;labelS,
     java.lang.String&nbsp;typS,
     java.util.List&lt;java.lang.String&gt;&nbsp;symList)
      throws <a href="../../mmj/lang/LangException.html" title="class in mmj.lang">LangException</a></pre>
<div class="block">Construct using a boatload of parameters.</div>
<dl><dt><span class="strong">Parameters:</span></dt><dd><code>seq</code> - MObj.seq number</dd><dd><code>scopeDefList</code> - the Scope list</dd><dd><code>symTbl</code> - Symbol Table (Map)</dd><dd><code>stmtTbl</code> - Statement Table (Map)</dd><dd><code>labelS</code> - Label String identifying the Assrt</dd><dd><code>typS</code> - Type Code String (first sym of formula)</dd><dd><code>symList</code> - Formula's Expression (2nd thru nth syms)</dd>
<dt><span class="strong">Throws:</span></dt>
<dd><code><a href="../../mmj/lang/LangException.html" title="class in mmj.lang">LangException</a></code> - variety of errors :)</dd></dl>
</li>
</ul>
</li>
</ul>
<!-- ============ METHOD DETAIL ========== -->
<ul class="blockList">
<li class="blockList"><a name="method_detail">
<!--   -->
</a>
<h3>Method Detail</h3>
<a name="getMandVarHypArray()">
<!--   -->
</a>
<ul class="blockList">
<li class="blockList">
<h4>getMandVarHypArray</h4>
<pre>public&nbsp;<a href="../../mmj/lang/VarHyp.html" title="class in mmj.lang">VarHyp</a>[]&nbsp;getMandVarHypArray()</pre>
<div class="block">Return the *mandatory* varHypArray.
 <p>
 Note: the "varHypArray" contains only *mandatory* VarHyp's, hence the
 name of this function, which is intended to highlight the point. These
 are the VarHyp's use in the Assrt's Formula.</div>
<dl>
<dt><strong>Specified by:</strong></dt>
<dd><code><a href="../../mmj/lang/Stmt.html#getMandVarHypArray()">getMandVarHypArray</a></code>&nbsp;in class&nbsp;<code><a href="../../mmj/lang/Stmt.html" title="class in mmj.lang">Stmt</a></code></dd>
<dt><span class="strong">Returns:</span></dt><dd>varHypArray which contains only mandatory VarHyp's.</dd></dl>
</li>
</ul>
<a name="getLogHypArray()">
<!--   -->
</a>
<ul class="blockList">
<li class="blockList">
<h4>getLogHypArray</h4>
<pre>public&nbsp;<a href="../../mmj/lang/LogHyp.html" title="class in mmj.lang">LogHyp</a>[]&nbsp;getLogHypArray()</pre>
<div class="block">Return the logHypArray.</div>
<dl><dt><span class="strong">Returns:</span></dt><dd>logHypArray for the Assrt.</dd></dl>
</li>
</ul>
<a name="getLogHypArrayLength()">
<!--   -->
</a>
<ul class="blockList">
<li class="blockList">
<h4>getLogHypArrayLength</h4>
<pre>public&nbsp;int&nbsp;getLogHypArrayLength()</pre>
<div class="block">Return the logHypArray length</div>
<dl><dt><span class="strong">Returns:</span></dt><dd>Assrt's logHypArray length.</dd></dl>
</li>
</ul>
<a name="setLogHypArray(mmj.lang.LogHyp[])">
<!--   -->
</a>
<ul class="blockList">
<li class="blockList">
<h4>setLogHypArray</h4>
<pre>public&nbsp;void&nbsp;setLogHypArray(<a href="../../mmj/lang/LogHyp.html" title="class in mmj.lang">LogHyp</a>[]&nbsp;logHypArray)</pre>
<div class="block">Set the logHypArray.</div>
<dl><dt><span class="strong">Parameters:</span></dt><dd><code>logHypArray</code> - for the Assrt.</dd></dl>
</li>
</ul>
<a name="getMandHypArrayLength()">
<!--   -->
</a>
<ul class="blockList">
<li class="blockList">
<h4>getMandHypArrayLength</h4>
<pre>public&nbsp;int&nbsp;getMandHypArrayLength()</pre>
<div class="block">Return the *mandatory* Hyp Array.Length</div>
<dl>
<dt><strong>Specified by:</strong></dt>
<dd><code><a href="../../mmj/lang/Stmt.html#getMandHypArrayLength()">getMandHypArrayLength</a></code>&nbsp;in class&nbsp;<code><a href="../../mmj/lang/Stmt.html" title="class in mmj.lang">Stmt</a></code></dd>
<dt><span class="strong">Returns:</span></dt><dd>hypArray length from the Assrt's MandFrame.</dd></dl>
</li>
</ul>
<a name="setMandVarHypArray(mmj.lang.VarHyp[])">
<!--   -->
</a>
<ul class="blockList">
<li class="blockList">
<h4>setMandVarHypArray</h4>
<pre>public&nbsp;void&nbsp;setMandVarHypArray(<a href="../../mmj/lang/VarHyp.html" title="class in mmj.lang">VarHyp</a>[]&nbsp;varHypArray)</pre>
<div class="block">Set the *mandatory* VarHyp Array.</div>
<dl><dt><span class="strong">Parameters:</span></dt><dd><code>varHypArray</code> - VarHyp's used by the Assrt.</dd></dl>
</li>
</ul>
<a name="getMandFrame()">
<!--   -->
</a>
<ul class="blockList">
<li class="blockList">
<h4>getMandFrame</h4>
<pre>public&nbsp;<a href="../../mmj/lang/ScopeFrame.html" title="class in mmj.lang">ScopeFrame</a>&nbsp;getMandFrame()</pre>
<div class="block">Get the Assrt's MandFrame.</div>
<dl><dt><span class="strong">Returns:</span></dt><dd>Assrt's MandFrame.</dd></dl>
</li>
</ul>
<a name="setMandFrame(mmj.lang.ScopeFrame)">
<!--   -->
</a>
<ul class="blockList">
<li class="blockList">
<h4>setMandFrame</h4>
<pre>public&nbsp;void&nbsp;setMandFrame(<a href="../../mmj/lang/ScopeFrame.html" title="class in mmj.lang">ScopeFrame</a>&nbsp;mandFrame)</pre>
<div class="block">Set the Assrt's MandFrame.</div>
<dl><dt><span class="strong">Parameters:</span></dt><dd><code>mandFrame</code> - Assrt's MandFrame.</dd></dl>
</li>
</ul>
<a name="isActive()">
<!--   -->
</a>
<ul class="blockList">
<li class="blockList">
<h4>isActive</h4>
<pre>public&nbsp;boolean&nbsp;isActive()</pre>
<div class="block">Is the Assrt "active".
 <p>
 Yep. Always. An assertion is always "active" even if it is defined inside
 a scope level. (Recall that, in practice, "active" simply means that a
 statement can be referred to by a subsequent statement in a proof or
 parse RPN.)
 <p>
 That is because Metmath "scope" is designed primarily to limit the
 visibility of hypotheses so that variables can be reused with different
 Types and so that logical hypotheses can be applied to just a single
 assertion. In a sense, Metamath scopes are merely notational shorthand,
 and as Metamath.pdf explains, every assertion has an "Extended Frame"
 (look it up for more info.)</div>
<dl>
<dt><strong>Specified by:</strong></dt>
<dd><code><a href="../../mmj/lang/Stmt.html#isActive()">isActive</a></code>&nbsp;in class&nbsp;<code><a href="../../mmj/lang/Stmt.html" title="class in mmj.lang">Stmt</a></code></dd>
<dt><span class="strong">Returns:</span></dt><dd>true (assertions are always "active")</dd></dl>
</li>
</ul>
<a name="loadLogHypArray()">
<!--   -->
</a>
<ul class="blockList">
<li class="blockList">
<h4>loadLogHypArray</h4>
<pre>public&nbsp;void&nbsp;loadLogHypArray()</pre>
<div class="block">Loads the logHypArray using mandFrame.
 <p>
 This is pretty redundant, but is an add-on for ProofAsst and is designed
 to be as bombproof as possible -- the output logHypArray is guaranteed to
 be in database sequence because it is created from MandFrame.hypArray.</div>
</li>
</ul>
<a name="accumHypInList(java.util.List,mmj.lang.Hyp)">
<!--   -->
</a><a name="accumHypInList(java.util.List, T)">
<!--   -->
</a>
<ul class="blockList">
<li class="blockList">
<h4>accumHypInList</h4>
<pre>public static&nbsp;&lt;T extends <a href="../../mmj/lang/Hyp.html" title="class in mmj.lang">Hyp</a>&gt;&nbsp;void&nbsp;accumHypInList(java.util.List&lt;T&gt;&nbsp;hypList,
                                  T&nbsp;hypNew)</pre>
<div class="block">Accumulate unique hypotheses (no duplicates), storing them in an array
 list in order of their appearance in the database.
 <p>
 The input "hypList" is updated with unique variable hypotheses in the
 expression.
 <p>
 Because hypList is maintained in database statement sequence order,
 hypList should either be empty (new) before the call, or already be in
 that order.</div>
<dl><dt><span class="strong">Type Parameters:</span></dt><dd><code>T</code> - the actual type of the list</dd><dt><span class="strong">Parameters:</span></dt><dd><code>hypList</code> - List of Hyp's, updated here.</dd><dd><code>hypNew</code> - Candidate Hyp to be added to hypList if not already there.</dd></dl>
</li>
</ul>
<a name="getLogHypsMaxDepth()">
<!--   -->
</a>
<ul class="blockList">
<li class="blockList">
<h4>getLogHypsMaxDepth</h4>
<pre>public&nbsp;int&nbsp;getLogHypsMaxDepth()</pre>
<div class="block">Dynamically computes, if needed, the larges maximum depth of parse trees
 of logHypArray, and caches the value for later use.</div>
<dl><dt><span class="strong">Returns:</span></dt><dd>greatest maxDepth of parse trees for logHypArray.</dd></dl>
</li>
</ul>
<a name="getLogHypsL1HiLoKey()">
<!--   -->
</a>
<ul class="blockList">
<li class="blockList">
<h4>getLogHypsL1HiLoKey</h4>
<pre>public&nbsp;java.lang.String&nbsp;getLogHypsL1HiLoKey()</pre>
<div class="block">Dynamically computes, if needed, the Hi and Lo keys of Level 1 (root) of
 parse trees of logHypArray, and caches the value for later use.</div>
<dl><dt><span class="strong">Returns:</span></dt><dd>Level 1 HiLoKey of parse trees for logHypArray.</dd></dl>
</li>
</ul>
<a name="sortListIntoArray(java.util.List, java.util.Comparator)">
<!--   -->
</a>
<ul class="blockList">
<li class="blockList">
<h4>sortListIntoArray</h4>
<pre>public static&nbsp;<a href="../../mmj/lang/Assrt.html" title="class in mmj.lang">Assrt</a>[]&nbsp;sortListIntoArray(java.util.List&lt;<a href="../../mmj/lang/Assrt.html" title="class in mmj.lang">Assrt</a>&gt;&nbsp;assrtList,
                        java.util.Comparator&lt;<a href="../../mmj/lang/Assrt.html" title="class in mmj.lang">Assrt</a>&gt;&nbsp;comparator)</pre>
<div class="block">Sorts a list of Assrt into an array.</div>
<dl><dt><span class="strong">Parameters:</span></dt><dd><code>assrtList</code> - List of Assrt to be sorted.</dd><dd><code>comparator</code> - Comparator to be used for the sort.</dd>
<dt><span class="strong">Returns:</span></dt><dd>Array of Assrt with size equal to the number of elements in the
         input list.</dd></dl>
</li>
</ul>
<a name="getSortedLogHypArray()">
<!--   -->
</a>
<ul class="blockListLast">
<li class="blockList">
<h4>getSortedLogHypArray</h4>
<pre>public&nbsp;<a href="../../mmj/lang/LogHyp.html" title="class in mmj.lang">LogHyp</a>[]&nbsp;getSortedLogHypArray()</pre>
<div class="block">Return the sortedLogHypArray.</div>
<dl><dt><span class="strong">Returns:</span></dt><dd>sortedLogHypArray for the Assrt.</dd></dl>
</li>
</ul>
</li>
</ul>
</li>
</ul>
</div>
</div>
<!-- ========= END OF CLASS DATA ========= -->
<!-- ======= START OF BOTTOM NAVBAR ====== -->
<div class="bottomNav"><a name="navbar_bottom">
<!--   -->
</a><a href="#skip-navbar_bottom" title="Skip navigation links"></a><a name="navbar_bottom_firstrow">
<!--   -->
</a>
<ul class="navList" title="Navigation">
<li><a href="../../overview-summary.html">Overview</a></li>
<li><a href="package-summary.html">Package</a></li>
<li class="navBarCell1Rev">Class</li>
<li><a href="package-tree.html">Tree</a></li>
<li><a href="../../deprecated-list.html">Deprecated</a></li>
<li><a href="../../index-all.html">Index</a></li>
<li><a href="../../help-doc.html">Help</a></li>
</ul>
</div>
<div class="subNav">
<ul class="navList">
<li>Prev Class</li>
<li><a href="../../mmj/lang/Axiom.html" title="class in mmj.lang"><span class="strong">Next Class</span></a></li>
</ul>
<ul class="navList">
<li><a href="../../index.html?mmj/lang/Assrt.html" target="_top">Frames</a></li>
<li><a href="Assrt.html" target="_top">No Frames</a></li>
</ul>
<ul class="navList" id="allclasses_navbar_bottom">
<li><a href="../../allclasses-noframe.html">All Classes</a></li>
</ul>
<div>
<script type="text/javascript"><!--
  allClassesLink = document.getElementById("allclasses_navbar_bottom");
  if(window==top) {
    allClassesLink.style.display = "block";
  }
  else {
    allClassesLink.style.display = "none";
  }
  //-->
</script>
</div>
<div>
<ul class="subNavList">
<li>Summary:&nbsp;</li>
<li>Nested&nbsp;|&nbsp;</li>
<li><a href="#field_summary">Field</a>&nbsp;|&nbsp;</li>
<li><a href="#constructor_summary">Constr</a>&nbsp;|&nbsp;</li>
<li><a href="#method_summary">Method</a></li>
</ul>
<ul class="subNavList">
<li>Detail:&nbsp;</li>
<li><a href="#field_detail">Field</a>&nbsp;|&nbsp;</li>
<li><a href="#constructor_detail">Constr</a>&nbsp;|&nbsp;</li>
<li><a href="#method_detail">Method</a></li>
</ul>
</div>
<a name="skip-navbar_bottom">
<!--   -->
</a></div>
<!-- ======== END OF BOTTOM NAVBAR ======= -->
</body>
</html>
